$\forall$$T$:Type, $L_{1}$,$L_{2}$:($T$ List), $x$,$y$:$T$.
\\[0ex]($\neg$($y$ $\in$ $L_{2}$)) $\Rightarrow$ l\_before($x$; $y$; append($L_{1}$; $L_{2}$); $T$) $\Rightarrow$ l\_before($x$; $y$; $L_{1}$; $T$)